$\forall$$A$:Type, ${\it es}$:ES, $I$:AbsInterface($A$), $P$:(E$\rightarrow\mathbb{P}$), $p$:($\forall$$e$:E. Dec($P$($e$))).
\\[0ex]($\forall$$e$:E. ($\uparrow$($e$ $\in_{b}$ $I$)) $\Rightarrow$ $P$($e$)) $\Rightarrow$ (($I$$\mid$$p$) = $I$)